$\forall$${\it es}$:ES\{i\}, $e$:E, ${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, $P$:(State(${\it ds}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $j$:Id. $e$:$s$.$P$($s$)@$j$  $\in$ Prop$_{\mbox{\scriptsize i'}}$